$\forall$$M$:MsgA, ${\it dec}$:($a$:Id$\rightarrow$$s$:$M$.state$\rightarrow$Dec($a$ in dom($M$.pre) \& ($\exists$$v$:$M$.da(locl($a$)). $M$.pre($a$,$s$,$v$)))).
\\[0ex]Chooser(${\it dec}$) $\in$ $b$:Id$\rightarrow$$M$.state$\rightarrow$($M$.da(locl($b$))+Unit)